/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ β'FORMALIZATION OF TWO PUZZLES INVOLVING KNOWLEDGE

␈↓ α∧␈↓␈↓ αTThis␈α
paper␈α
describes␈α
a␈α
formal␈α
system␈α
and␈α
uses␈α
it␈α
to␈α
express␈α
the␈α
puzzle␈α
of␈α
the␈α
three␈αwise␈α
men
␈↓ α∧␈↓and␈αthe␈α
puzzle␈αof␈αMr.␈α
S␈αand␈α
Mr.␈αP.␈α Four␈α
innovations␈αin␈αthe␈α
axiomatization␈αof␈α
knowledge␈αwere
␈↓ α∧␈↓required:␈αthe␈αability␈αto␈αexpress␈αjoint␈αknowledge␈αof␈αseveral␈αpeople,␈αthe␈αability␈αto␈αexpress␈αthe␈αinitial
␈↓ α∧␈↓non-knowledge,␈α∞the␈α
ability␈α∞to␈α
describe␈α∞knowing␈α
what␈α∞rather␈α
than␈α∞merely␈α
knowing␈α∞that,␈α∞and␈α
the
␈↓ α∧␈↓ability␈α⊂to␈α⊂express␈α⊂the␈α⊂change␈α⊂which␈α⊂occurs␈α⊂when␈α⊂someone␈α⊂learns␈α⊂something.␈α⊂ Our␈α⊂axioms␈α⊂are
␈↓ α∧␈↓written␈α∩in␈α∩first␈α∩order␈α∪logic␈α∩and␈α∩use␈α∩Kripke-style␈α∪possible␈α∩worlds␈α∩directly␈α∩rather␈α∪than␈α∩modal
␈↓ α∧␈↓operators␈αor␈αimitations␈αthereof.␈α We␈αintend␈αto␈αuse␈αfunctions␈αimitating␈αmodal␈αoperators␈αand␈αtaking
␈↓ α∧␈↓"propositions"␈α∞and␈α∞"individual␈α∞concepts"␈α
as␈α∞operands,␈α∞but␈α∞we␈α
haven't␈α∞yet␈α∞solved␈α∞the␈α∞problem␈α
of
␈↓ α∧␈↓how to treat learning in such a formalism.

␈↓ α∧␈↓␈↓ αTThe puzzles to be treated are the following:


␈↓ α∧␈↓αThe three wise men

␈↓ α∧␈↓␈↓ αT␈↓↓"A␈αcertain␈αking␈αwishes␈αto␈αtest␈αhis␈αthree␈αwise␈αmen.␈α He␈αarranges␈αthem␈αin␈αa␈αcircle␈αso␈αthat␈αthey
␈↓ α∧␈↓↓can␈α
see␈αand␈α
hear␈αeach␈α
other␈α
and␈αtells␈α
them␈αthat␈α
he␈αwill␈α
put␈α
a␈αwhite␈α
or␈αblack␈α
spot␈αon␈α
each␈α
of␈αtheir
␈↓ α∧␈↓↓foreheads␈α∂but␈α∂that␈α⊂at␈α∂least␈α∂one␈α∂spot␈α⊂will␈α∂be␈α∂white.␈α⊂ In␈α∂fact␈α∂all␈α∂three␈α⊂spots␈α∂are␈α∂white.␈α⊂ He␈α∂then
␈↓ α∧␈↓↓repeatedly asks them, "Do you know the cclor of your spot".  What do they answer?"␈↓

␈↓ α∧␈↓␈↓ αTThe␈αsolution␈αis␈αthat␈αthey␈αanswer,␈α␈↓↓"No"␈↓,␈αthe␈αfirst␈αtwo␈αtimes␈αthe␈αquestion␈αis␈αasked␈αand␈αanswer
␈↓ α∧␈↓␈↓↓"Yes"␈↓ thereafter.

␈↓ α∧␈↓␈↓ αTThis is a variant form of the puzzle.  The traditional form is

␈↓ α∧␈↓␈↓ αT␈↓↓"A␈αcertain␈αking␈αwishes␈αto␈αdetermine␈αwhich␈α
of␈αhis␈αthree␈αwise␈αmen␈αis␈αthe␈αwisest.␈α
 He␈αarranges
␈↓ α∧␈↓↓them␈αin␈αa␈αcircle␈αso␈αthat␈αthey␈αcan␈αsee␈αand␈αhear␈αeach␈αother␈αand␈αtells␈αthem␈αthat␈αhe␈αwill␈αput␈αa␈αwhite␈αor
␈↓ α∧␈↓↓black␈αspot␈αon␈αeach␈αof␈αtheir␈α
foreheads␈αbut␈αthat␈αat␈αleast␈αone␈αspot␈α
will␈αbe␈αwhite.␈α In␈αfact␈αall␈αthree␈α
spots
␈↓ α∧␈↓↓are␈αwhite.␈α He␈αthen␈αoffers␈αhis␈αfavor␈αto␈αthe␈αone␈αwho␈αwill␈αfirst␈αtell␈αhim␈αthe␈αcolor␈αof␈αhis␈αspot.␈α After␈αa
␈↓ α∧␈↓↓while, the wisest announces that his spot his white.  How does he know?"␈↓

␈↓ α∧␈↓␈↓ αTThe␈α⊂intended␈α⊂solution␈α∂is␈α⊂that␈α⊂the␈α∂wisest␈α⊂reasons␈α⊂that␈α∂if␈α⊂his␈α⊂spot␈α∂were␈α⊂black,␈α⊂the␈α∂second
␈↓ α∧␈↓would␈α
see␈αa␈α
black␈αand␈α
a␈α
white␈αand␈α
would␈αreason␈α
that␈αif␈α
his␈α
spot␈αwere␈α
black,␈αthe␈α
third␈αwould␈α
have
␈↓ α∧␈↓seen␈α
two␈α∞black␈α
spot␈α∞and␈α
reasoned␈α∞from␈α
the␈α∞king's␈α
announcement␈α∞that␈α
his␈α∞spot␈α
was␈α∞white.␈α
 This
␈↓ α∧␈↓traditional␈αversion␈α
requires␈αthe␈αwise␈α
men␈αto␈α
reason␈αabout␈αhow␈α
fast␈αtheir␈α
colleagues␈αreason,␈αand␈α
we
␈↓ α∧␈↓don't wish to try to formalize this.


␈↓ α∧␈↓αMr. S and Mr. P

␈↓ α∧␈↓␈↓ αT␈↓↓Two␈α∞numbers␈α
m␈α∞and␈α
n␈α∞are␈α
chosen␈α∞such␈α
that␈α∞2 ≤ m ≤ n ≤ 99.␈α
 Mr.␈α∞S␈α
is␈α∞told␈α
their␈α∞sum␈α
and
␈↓ α∧␈↓↓Mr. P is told their product.  The following dialogue ensues:

␈↓ α∧␈↓␈↓↓Mr. P: I don't know the numbers.

␈↓ α∧␈↓↓Mr. S: I knew you didn't know.  I don't know either.

␈↓ α∧␈↓↓Mr. P: Now I know the numbers.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓↓Mr. S: Now I know them too.

␈↓ α∧␈↓↓In view of the above dialogue, what are the numbers?"␈↓


␈↓ α∧␈↓αSimple axiomatization of the wise men

␈↓ α∧␈↓␈↓ αTIf␈α
we␈α
can␈α
assume␈α
that␈α
the␈α
first␈α
and␈α
second␈α
wisemen␈α
don't␈α
know␈α
the␈α
colors␈α
of␈α
their␈αspots,␈α
that
␈↓ α∧␈↓the␈α⊗second␈α⊗knows␈α⊗that␈α⊗the␈α⊗first␈α⊗doesn't␈α∃know,␈α⊗and␈α⊗the␈α⊗third␈α⊗knows␈α⊗this,␈α⊗then␈α⊗a␈α∃simple
␈↓ α∧␈↓axiomatization that doesn't explicitly treat learning works.

␈↓ α∧␈↓[In␈α
this␈α
draft,␈α
we␈α
omit␈α
this␈α
section.␈α Instead␈α
we␈α
include␈α
an␈α
older␈α
self-contained␈α
memo␈αwritten␈α
when
␈↓ α∧␈↓this was our main approach to the problem].


␈↓ α∧␈↓αFull axiomatization of the wise men

␈↓ α∧␈↓␈↓ αTThe␈α
axioms␈α
are␈α
given␈α
in␈α
a␈α
form␈α
acceptable␈α
to␈α
FOL,␈α
the␈α
proof␈α
checker␈α
computer␈αprogram
␈↓ α∧␈↓for␈α
an␈α
extended␈α
first␈α
order␈α
logic␈α
at␈α
the␈α
Stanford␈α
Artificial␈α
Intelligence␈α
Laboratory.␈α
 FOL␈α∞uses␈α
a
␈↓ α∧␈↓sorted␈αlogic␈α
and␈αconstants␈αand␈α
variables␈αare␈α
declared␈αto␈αhave␈α
given␈αsorts,␈α
and␈αquantifiers␈αon␈α
these
␈↓ α∧␈↓variables are interpreted as ranging over the sorts corresponding to the variables.

␈↓ α∧␈↓␈↓ αTThe axiomatization has the following features:

␈↓ α∧␈↓␈↓ αT1. It is entirely in first order logic rather than in a modal logic.

␈↓ α∧␈↓␈↓ αT2.␈α
The␈α
Kripke␈α
accessibility␈α
relation␈α∞is␈α
axiomatized.␈α
 No␈α
knowledge␈α
operator␈α
or␈α∞function␈α
is
␈↓ α∧␈↓used.␈α
 We␈α
hope␈α
to␈α
present␈α
a␈α
second␈αaxiomatization␈α
using␈α
a␈α
knowledge␈α
function,␈α
but␈α
we␈αhaven't␈α
yet
␈↓ α∧␈↓decided how to handle time and learning in such an axiomatization.

␈↓ α∧␈↓␈↓ αT3.␈α
We␈α
are␈α
essentially␈α
treating␈α
"knowing␈α∞what"␈α
rather␈α
than␈α
"knowing␈α
that".␈α
 We␈α
say␈α∞that␈α
p
␈↓ α∧␈↓knows␈αthe␈αcolor␈αof␈αhis␈αspot␈αin␈αworld␈αw␈αby␈αsaying␈αthat␈αin␈αall␈αworlds␈αaccessible␈αfrom␈αw,␈αthe␈αcolor␈αof
␈↓ α∧␈↓the spot is the same as in w.

␈↓ α∧␈↓␈↓ αT4.␈α⊂We␈α⊂treat␈α⊂learning␈α⊂by␈α⊂giving␈α⊃the␈α⊂accessibility␈α⊂relation␈α⊂a␈α⊂time␈α⊂parameter.␈α⊂ To␈α⊃say␈α⊂that
␈↓ α∧␈↓someone␈αlearns␈αsomething␈αis␈αdone␈αby␈αsaying␈αthat␈αthe␈αworlds␈αaccessible␈αto␈αhim␈αat␈αtime␈αn+1␈αare␈αthe
␈↓ α∧␈↓subset of those accessible at time n in which the something is true.

␈↓ α∧␈↓␈↓ αT5.␈α∂The␈α∂problems␈α∂treated␈α∂are␈α∂complicated␈α∂by␈α∂the␈α∂need␈α∂to␈α∂treat␈α∂joint␈α∂knowledge␈α∂and␈α∂joint
␈↓ α∧␈↓learning.␈α This␈αis␈αdone␈αby␈αintroducing␈αfictitious␈αpersons␈αwho␈αknow␈αwhat␈αa␈αgroup␈αof␈αpeople␈αknow
␈↓ α∧␈↓jointly.

␈↓ α∧␈↓␈↓ αTdeclare INDCONST RW ε WORLD;
␈↓ α∧␈↓␈↓ αTdeclare INDVAR w w1 w2 w3 w4 w5 ε WORLD;

␈↓ α∧␈↓␈↓ αTRW denotes the real world, and w, w1, ... , w5 are variables ranging over worlds.

␈↓ α∧␈↓␈↓ αTdeclare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

␈↓ α∧␈↓␈↓ αTWe use natural numbers for times.
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓␈↓ αTdeclare INDCONST W1 W2 W3 W123 ε PERSON;
␈↓ α∧␈↓␈↓ αTdeclare INDVAR p p0 p1 p2 ε PERSON;

␈↓ α∧␈↓␈↓ αTW1,␈αW2␈αand␈αW3␈αare␈αthe␈αthree␈αwisemen.␈α W123␈αis␈αa␈αfictitious␈αperson␈αwho␈αknows␈αwhatever
␈↓ α∧␈↓W1,␈αW2␈αand␈αW3␈αknow␈αjointly.␈α The␈αjoint␈αknowledge␈αof␈αseveral␈αpeople␈αis␈αtypified␈αby␈αevents␈αthat
␈↓ α∧␈↓occur␈α
in␈α
their␈α
joint␈α
presence.␈α
 Not␈αonly␈α
do␈α
they␈α
all␈α
know␈α
it,␈αbut␈α
W1␈α
knows␈α
that␈α
W2␈α
knows␈αthat
␈↓ α∧␈↓W1␈αknows␈αthat␈αW3␈αknows␈αetc.␈α Instead␈αof␈αintroducing␈αW123,␈αwe␈αcould␈αintroduce␈αprefixes␈αof␈αlike
␈↓ α∧␈↓"W1 knows that W2 knows" as objects and quantify over prefixes.

␈↓ α∧␈↓␈↓ αTdeclare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

␈↓ α∧␈↓␈↓ αTThis␈α
Kripke-style␈α
accessibility␈αrelation␈α
has␈α
two␈αmore␈α
arguments␈α
than␈αis␈α
usual␈α
in␈αmodal␈α
logic
␈↓ α∧␈↓- a person and a time.

␈↓ α∧␈↓␈↓ αTdeclare INDVAR c c1 c2 c3 c4 ε COLORS;
␈↓ α∧␈↓␈↓ αTdeclare INDCONST W B ε COLORS;

␈↓ α∧␈↓␈↓ αTThere are two colors - white and black.

␈↓ α∧␈↓␈↓ αTdeclare OPCONST color(PERSON,WORLD) = COLORS;

␈↓ α∧␈↓␈↓ αTA␈αperson␈α
has␈αa␈αcolor␈α
in␈αa␈αworld.␈α
 Note␈αthat␈αthe␈α
previous␈αaxiomatization␈αwas␈α
simpler.␈α We
␈↓ α∧␈↓merely␈αhad␈αthree␈αpropositions␈αWISE1,␈αWISE2␈αand␈αWISE3␈αasserting␈αthat␈αthe␈αrespective␈αwise␈αmen
␈↓ α∧␈↓had white spots.  We need the colors, because we want to quantify over colors.

␈↓ α∧␈↓␈↓ αTaxiom reflex: ∀w p m.A(w,w,p,m);;

␈↓ α∧␈↓␈↓ αTThe accessibility relation is reflexive as is usual in Kripke the semantics of M.

␈↓ α∧␈↓␈↓ αTaxiom transitive: ∀w1 w2 w3 p m.(A(w1,w2,p,m) ∧ A(w2,w3,p,m) ⊃ A(w1,w3,p,m));;

␈↓ α∧␈↓␈↓ αTMaking␈α
the␈α
accessibility␈α
relation␈α
transitive␈α
gives␈αan␈α
S4␈α
like␈α
system.␈α
 We␈α
use␈α
transitivity␈αin
␈↓ α∧␈↓the proof, but we aren't sure it is necessary.

␈↓ α∧␈↓␈↓ αTaxiom who: ∀p.(p=W1 ∨ p=W2 ∨ p=W3 ∨ p=W123);;

␈↓ α∧␈↓␈↓ αTWe need to delimit the set of wise men.

␈↓ α∧␈↓␈↓ αTaxiom␈α≥w123:␈α≡∀w1␈α≥w2␈α≥m.(A(w1,w2,W1,m)␈α≡∨␈α≥A(w1,w2,W2,m)␈α≥∨␈α≡A(w1,w2,W3,m)␈α≥⊃
␈↓ α∧␈↓A(w1,w2,W123,m));;

␈↓ α∧␈↓␈↓ αTThis says that anything the wise men know jointly, they know individually.

␈↓ α∧␈↓␈↓ αTaxiom foolspot: ∀w.(color(W123,w)=W);;

␈↓ α∧␈↓␈↓ αTThis␈α
ad␈α
hoc␈α
axiom␈α
is␈α
the␈α∞penalty␈α
for␈α
introducing␈α
W123␈α
as␈α
an␈α
ordinary␈α∞individual␈α
whose
␈↓ α∧␈↓spot␈α
must␈αtherefore␈α
have␈αa␈α
color.␈α It␈α
would␈αhave␈α
been␈αbetter␈α
to␈αdistinguish␈α
between␈α
real␈αpersons
␈↓ α∧␈↓with␈α
spots␈α
and␈α
the␈α
fictitious␈α
person(s)␈α
who␈αonly␈α
know␈α
things.␈α
 Anyway,␈α
we␈α
give␈α
W123␈α
a␈αwhite␈α
spot
␈↓ α∧␈↓and make it generally known, e.g. true in all possible worlds.
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓␈↓ αTaxiom color:    ¬(W=B)
␈↓ α∧␈↓␈↓ αT                ∀c.(c=W ∨ c=B)
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTBoth of these axioms about the colors are used in the proof.

␈↓ α∧␈↓␈↓ αTaxiom rw: color(W1,RW) = W ∧ color(W2,RW) = W ∧ color(W3,RW) = W;;

␈↓ α∧␈↓␈↓ αTIn fact all spots are white.

␈↓ α∧␈↓␈↓ αTaxiom king: ∀w.(A(RW,w,W123,0) ⊃ color(W1,w)=W ∨ color(W2,w)=W ∨ color(W3,w)=W);;

␈↓ α∧␈↓␈↓ αTThey␈α
jointly␈α∞know␈α
that␈α∞at␈α
least␈α
one␈α∞spot␈α
is␈α∞white,␈α
since␈α
the␈α∞king␈α
stated␈α∞it␈α
in␈α∞their␈α
mutual
␈↓ α∧␈↓presence.  We use the consequence that W3 knows that W2 knows that W1 knows this fact.

␈↓ α∧␈↓␈↓ αTaxiom initial:  ∀c w.(A(RW,w,W123,0) ⊃
␈↓ α∧␈↓␈↓ αT(c=W ∨ color(W2,w)=W ∨ color(W3,w)=W
␈↓ α∧␈↓␈↓ αT                ⊃ ∃w1.(A(w,w1,W1,0) ∧ color(W1,w1) = c)) ∧
␈↓ α∧␈↓␈↓ αT(c=W ∨ color(W1,w)=W ∨ color(W3,w)=W
␈↓ α∧␈↓␈↓ αT                ⊃ ∃w1.(A(w,w1,W2,0) ∧ color(W2,w1) = c)) ∧
␈↓ α∧␈↓␈↓ αT(c=W ∨ color(W1,w)=W ∨ color(W2,w)=W
␈↓ α∧␈↓␈↓ αT                ⊃ ∃w1.(A(w,w1,W3,0) ∧ color(W3,w1) = c)))

␈↓ α∧␈↓␈↓ αT∀w␈α∞w1.(A(RW,w,W123,0)␈α∞∧␈α
A(w,w1,W1,0)␈α∞⊃␈α∞color(W2,w1)␈α
=␈α∞color(W2,w)␈α∞∧␈α∞color(W3,w1)␈α
=
␈↓ α∧␈↓color(W3,w))

␈↓ α∧␈↓␈↓ αT∀w␈α∞w1.(A(RW,w,W123,0)␈α∞∧␈α
A(w,w1,W2,0)␈α∞⊃␈α∞color(W1,w1)␈α
=␈α∞color(W1,w)␈α∞∧␈α∞color(W3,w1)␈α
=
␈↓ α∧␈↓color(W3,w))

␈↓ α∧␈↓␈↓ αT∀w␈α⊃w1.(A(RW,w,W123,0)␈α⊃∧␈α⊃A(w,w1,W3,0)␈α⊃color(W1,w1)␈α⊃=␈α⊃color(W1,w)␈α⊃∧␈α∩color(W2,w1)␈α⊃=
␈↓ α∧␈↓color(W2,w)) ;;

␈↓ α∧␈↓␈↓ αTThese␈αare␈α
actually␈αfour␈α
axioms.␈α The␈αlast␈α
three␈αsay␈α
that␈αevery␈αone␈α
knows␈αthat␈α
each␈αknows
␈↓ α∧␈↓the␈α∂colors␈α∞of␈α∂the␈α∞other␈α∂men's␈α∞spots.␈α∂ The␈α∞first␈α∂part␈α∞says␈α∂that␈α∞they␈α∂all␈α∞know␈α∂that␈α∂no-one␈α∞knows
␈↓ α∧␈↓anything␈αmore␈αthan␈αwhat␈αhe␈αcan␈αsee␈αand␈αwhat␈αthe␈αking␈αtold␈αthem.␈α We␈αestablish␈αnon-knowledge
␈↓ α∧␈↓by␈α⊃asserting␈α∩the␈α⊃existence␈α⊃of␈α∩enough␈α⊃possible␈α⊃worlds.␈α∩ The␈α⊃ability␈α⊃to␈α∩quantify␈α⊃over␈α∩colors␈α⊃is
␈↓ α∧␈↓convenient␈α∞for␈α
expressing␈α∞this␈α
axiom␈α∞in␈α∞a␈α
natural␈α∞way.␈α
 In␈α∞the␈α∞S␈α
and␈α∞P␈α
problem␈α∞it␈α∞is␈α
essential,
␈↓ α∧␈↓because we would otherwise need a conjunction of 4753 terms.

␈↓ α∧␈↓␈↓ αTaxiom␈α∨elwek1:␈α≡∀w.(A(RW,w,W123,1)␈α∨≡␈α≡A(RW,w,W123,0)␈α∨∧␈α∨∀p.(∀w1.(A(w,w1,p,0)␈α≡⊃
␈↓ α∧␈↓color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,0) ⊃ color(p,w1)=color(p,RW))))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,W1,1) ≡ A(w1,w2,W1,0) ∧ A(w1,w2,W123,1))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,W2,1) ≡ A(w1,w2,W2,0) ∧ A(w1,w2,W123,1))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,W3,1) ≡ A(w1,w2,W3,0) ∧ A(w1,w2,W123,1)) ;;

␈↓ α∧␈↓␈↓ αTThis␈α
axiom␈α
and␈αthe␈α
next␈α
one␈αare␈α
the␈α
same␈αexcept␈α
that␈α
one␈αdeals␈α
with␈α
the␈α
transition␈αfrom
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓time␈α
0␈α
to␈α
time␈α
1␈α
and␈αthe␈α
other␈α
deals␈α
with␈α
the␈α
transition␈α
from␈αtime␈α
1␈α
to␈α
time␈α
2.␈α
 Each␈α
says␈αthat␈α
they
␈↓ α∧␈↓jointly␈αlearn␈αwho␈α(if␈αanyone)␈αknows␈αthe␈αcolor␈αof␈αhis␈αspot.␈α The␈αquantifier␈α∀p␈αin␈αthis␈αaxiom␈α
covers
␈↓ α∧␈↓W123 also and forced us to say that they jointly know the color of W123's spot.

␈↓ α∧␈↓␈↓ αTaxiom␈α∨elwek2:␈α≡∀w.(A(RW,w,W123,2)␈α∨≡␈α≡A(RW,w,W123,1)␈α∨∧␈α∨∀p.(∀w1.(A(w,w1,p,1)␈α≡⊃
␈↓ α∧␈↓color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,1) ⊃ color(p,w1)=color(p,RW))))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,W1,2) ≡ A(w1,w2,W1,1) ∧ A(w1,w2,W123,1))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,W2,2) ≡ A(w1,w2,W2,1) ∧ A(w1,w2,W123,1))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,W3,2) ≡ A(w1,w2,W3,1) ∧ A(w1,w2,W123,1)) ;;

␈↓ α∧␈↓␈↓ αTThe␈α∂file␈α∂WISEMA.PRF[S78,JMC]␈α∂at␈α∂the␈α∂Stanford␈α∂AI␈α∂Lab␈α∂contains␈α∂a␈α∂computer␈α∞checked
␈↓ α∧␈↓proof from these axioms of

␈↓ α∧␈↓␈↓ αT∀w.(A(RW,w,W3,2) ⊃ color(W3,w) = color(W3,RW))

␈↓ α∧␈↓␈↓ αTwhich␈α
is␈α
the␈α
assertion␈α
that␈α
at␈α
time␈α
2,␈α
the␈α
third␈α
wise␈α
man␈α
knows␈α
the␈α
color␈α
of␈α
his␈α∞spot.␈α
 As
␈↓ α∧␈↓intermediate␈α
results␈αwe␈α
had␈α
to␈αprove␈α
that␈αprevious␈α
to␈α
time␈α2,␈α
the␈αother␈α
wise␈α
men␈αdid␈α
not␈αknow␈α
the
␈↓ α∧␈↓colors␈α
of␈α∞their␈α
spots.␈α∞ In␈α
this␈α
symmetrical␈α∞axiomatization,␈α
we␈α∞could␈α
have␈α
made␈α∞the␈α
proof␈α∞with␈α
a
␈↓ α∧␈↓variable wise man instead of the constant W3.


␈↓ α∧␈↓α␈↓ αTAxiomatization of Mr. S and Mr. P

␈↓ α∧␈↓␈↓ αTThese␈α
axioms␈α
involve␈α
the␈α
same␈α
ideas␈α∞as␈α
the␈α
second␈α
wise␈α
man␈α
axiomatization.␈α
 In␈α∞fact,␈α
we
␈↓ α∧␈↓derived them first.

␈↓ α∧␈↓␈↓ αTdeclare INDCONST m0 n0 ε NATNUM;
␈↓ α∧␈↓␈↓ αTdeclare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

␈↓ α∧␈↓␈↓ αTdeclare INDCONST RW ε WORLD;
␈↓ α∧␈↓␈↓ αTdeclare INDVAR w w1 w2 w3 ε WORLD;

␈↓ α∧␈↓␈↓ αTdeclare OPCONST M(WORLD) = NATNUM;
␈↓ α∧␈↓␈↓ αTdeclare OPCONST N(WORLD) = NATNUM;

␈↓ α∧␈↓␈↓ αTdeclare INDCONST S P SP ε PERSON;
␈↓ α∧␈↓␈↓ αTdeclare INDVAR s s0 s1 s2 ε PERSON;

␈↓ α∧␈↓␈↓ αTdeclare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);
␈↓ α∧␈↓␈↓ αTdeclare PREDCONST ok(NATNUM,NATNUM);

␈↓ α∧␈↓␈↓ αTdeclare PREDCONST agree(WORLD,WORLD);

␈↓ α∧␈↓␈↓ αTdeclare PREDPAR phi(WORLD,WORLD);

␈↓ α∧␈↓␈↓ αTCOMMENT : The predicate agree is used to abbreviate subsequent axioms. :
␈↓ α∧␈↓␈↓ u6


␈↓ α∧␈↓␈↓ αTaxiom agree:    ∀w1 w2.(agree(w1,w2) ≡ M(w1) = M(w2) ∧ N(w1) = N(w2));;

␈↓ α∧␈↓␈↓ αTaxiom reflex:   ∀w s m.A(w,w,s,m);;

␈↓ α∧␈↓␈↓ αTaxiom transitive:       ∀w1 w2 w3 s m.(A(w1,w2,s,m) ∧ A(w2,w3,s,m) ⊃ A(w1,w3,s,m));;

␈↓ α∧␈↓␈↓ αTCOMMENT : The axiom sp characterizes the fictious person SP as knowing
␈↓ α∧␈↓␈↓ αTwhat S and P know jointly, i.e. S knows that P knows that S knows, etc. :

␈↓ α∧␈↓␈↓ αTaxiom sp:       ∀w1 w2 m.(A(w1,w2,S,m) ∨ A(w1,w2,P,m) ⊃ A(w1,w2,SP,m))

␈↓ α∧␈↓␈↓ αT                ∀m.(
␈↓ α∧␈↓␈↓ αT                ∀w1 w2.(A(w1,w2,S,m) ∨ A(w1,w2,P,m) ⊃ phi(w1,w2)) ∧
␈↓ α∧␈↓␈↓ αT                ∀w1 w2 w3.(phi(w1,w2) ∧ phi(w2,w3) ⊃ phi(w1,w3))
␈↓ α∧␈↓␈↓ αT⊃       ∀w1 w2.(phi(w1,w2) ⊃ A(w1,w2,SP,m)))
␈↓ α∧␈↓␈↓ αT;;


␈↓ α∧␈↓␈↓ αTaxiom rw:       m0 = M(RW)
␈↓ α∧␈↓␈↓ αT                n0 = N(RW)
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTaxiom ok:       ∀m n.(ok(m,n) ≡ 1<m ∧ 1<n ∧ m≤n ∧ m<100 ∧ n<100)
␈↓ α∧␈↓␈↓ αT                ∀w.ok(M(w),N(w))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : initial establishes the existence of enough possible worlds
␈↓ α∧␈↓␈↓ αTto express that S and P initially know only what follows from their
␈↓ α∧␈↓␈↓ αTknowledge of the sum and product respectively, and that they jointly
␈↓ α∧␈↓␈↓ αTknow this ignorance. :

␈↓ α∧␈↓␈↓ αTaxiom initial:
␈↓ α∧␈↓␈↓ αT∀w w1.(A(RW,w,SP,0) ∧ A(w,w1,S,0) ⊃ M(w1)+N(w1) = M(w)+N(w))
␈↓ α∧␈↓␈↓ αT∀w w1.(A(RW,w,SP,0) ∧ A(w,w1,P,0) ⊃ M(w1)*N(w1) = M(w)*N(w))
␈↓ α∧␈↓␈↓ αT∀w m n.(A(RW,w,SP,0) ∧ ok(m,n) ∧ M(w) + N(w) = m + n ⊃
␈↓ α∧␈↓␈↓ αT∃w1.(A(w,w1,S,0) ∧ M(w1) = m ∧ N(w1) = n))
␈↓ α∧␈↓␈↓ αT∀w m n.(A(RW,w,SP,0) ∧ ok(m,n) ∧ M(w) * N(w) = m * n ⊃
␈↓ α∧␈↓␈↓ αT∃w1.(A(w,w1,P,0) ∧ M(w1) = m ∧ N(w1) = n))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : Mr. P doesn't know the numbers. :

␈↓ α∧␈↓␈↓ αTaxiom npk:
␈↓ α∧␈↓␈↓ αT∃w.(A(RW,w,P,0) ∧ ¬agree(RW,w))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : Mr. S knew that Mr. P didn't know. :

␈↓ α∧␈↓␈↓ αTaxiom sknpk:
␈↓ α∧␈↓␈↓ αT∀w.(A(RW,w,S,0) ⊃ ∃w1.(A(w,w1,P,0) ∧ ¬agree(w,w1)))
␈↓ α∧␈↓␈↓ u7


␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : Mr. S doesn't know either. :

␈↓ α∧␈↓␈↓ αTaxiom nsk:
␈↓ α∧␈↓␈↓ αT∃w.(A(RW,w,S,0) ∧ ¬agree(RW,w))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : They jointly learn that Mr. S knows that Mr. P doesn't know and
␈↓ α∧␈↓␈↓ αTthat Mr. S doesn't know either. :

␈↓ α∧␈↓␈↓ αTaxiom elsknpkansk:
␈↓ α∧␈↓␈↓ αT∀w.(A(RW,w,SP,1) ≡ A(RW,w,SP,0) ∧
␈↓ α∧␈↓␈↓ αT∀w1.(A(w,w1,S,0) ⊃ ∃w2.(A(w1,w2,P,0) ∧ ¬agree(w1,w2))) ∧
␈↓ α∧␈↓␈↓ αT∃w1.(A(w,w1,S,0) ∧ ¬agree(w,w1)))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,S,1) ≡ A(w1,w2,S,0) ∧ A(w1,w2,SP,1))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,P,1) ≡ A(w1,w2,P,0) ∧ A(w1,w2,SP,1))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : In this new situation, Mr. P knows the numbers. :

␈↓ α∧␈↓␈↓ αTaxiom pk:
␈↓ α∧␈↓␈↓ αT∀w.(A(RW,w,P,1) ⊃ agree(RW,w))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : Everyone learns that Mr. P now knows. :

␈↓ α∧␈↓␈↓ αTaxiom elpk:
␈↓ α∧␈↓␈↓ αT∀w.(A(RW,w,SP,2) ≡ A(RW,w,SP,1)
␈↓ α∧␈↓␈↓ αT∧ ∀w1.(A(w,w1,P,1) ⊃ agree(w,w1)))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,S,2) ≡ A(w1,w2,S,1) ∧ A(w1,w2,SP,2))

␈↓ α∧␈↓␈↓ αT∀w1 w2.(A(w1,w2,P,2) ≡ A(w1,w2,P,1) ∧ A(w1,w2,SP,2))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTCOMMENT : In this new situation Mr. S knows too. :

␈↓ α∧␈↓␈↓ αTaxiom sk:       ∀w.(A(RW,w,S,2) ⊃ agree(RW,w));;
␈↓ α∧␈↓␈↓ αTCOMMENT : The following are purely arithmetic definitions and are intended
␈↓ α∧␈↓␈↓ αTto be used in expressing the translation of the problem from the
␈↓ α∧␈↓␈↓ αTmodal form to a purely arithmetic form.  Completing the proof
␈↓ α∧␈↓␈↓ αTthat m0 = 4 and n0 = 13 will require
␈↓ α∧␈↓␈↓ αTusing a set of axioms for arithmetic, but that is not of interest here :

␈↓ α∧␈↓␈↓ αTdeclare PREDCONST R0(NATNUM,NATNUM) R1(NATNUM,NATNUM)
␈↓ α∧␈↓␈↓ αTR2(NATNUM,NATNUM) R3(NATNUM,NATNUM);
␈↓ α∧␈↓␈↓ u8


␈↓ α∧␈↓␈↓ αTaxiom R0:       ∀m n.(R0(m,n) ≡ ok(m,n) ∧ ∃m1 n1.(ok(m1,n1) ∧ m1*n1 = m*n
␈↓ α∧␈↓␈↓ αT∧ ¬(m1=m ∧ n1=n)))
␈↓ α∧␈↓␈↓ αT;;

␈↓ α∧␈↓␈↓ αTaxiom R1:       ∀m n.(R1(m,n) ≡ ok(m,n) ∧
␈↓ α∧␈↓␈↓ αT                        ∀m1 n1.(ok(m1,n1) ∧ m1+n1 = m+n ⊃ R0(m1,n1)) ∧
␈↓ α∧␈↓␈↓ αT                        ∃m1 n1.(m1+n1 = m+n ∧ ¬(m1=m ∧ n1=n)));;


␈↓ α∧␈↓␈↓ αTaxiom R2:       ∀m n.(R2(m,n) ≡ ok(m,n) ∧
␈↓ α∧␈↓␈↓ αT                        ∀m1 n1.(m1*n1 = m*n ∧ R1(m1,n1) ⊃ m1=m ∧ n1=n));;

␈↓ α∧␈↓␈↓ αTaxiom R3:       ∀m n.(R3(m,n) ≡ ok(m,n) ∧
␈↓ α∧␈↓␈↓ αT                        ∀m1 n1.(m1+n1 = m+n ∧ R2(m1,n1) ⊃ m1=m ∧ n1=n));;


␈↓ α∧␈↓␈↓ αTWe␈α
should␈α
be␈αable␈α
to␈α
prove␈α␈↓↓R3(m0,n0)␈↓␈α
from␈α
the␈α
above␈αaxioms.␈α
 The␈α
subsequent␈αproof␈α
that
␈↓ α∧␈↓␈↓↓m0 = 4 ∧ n0 = 13␈↓ should not involve the knowledge axioms and should be purely arithmetic.

␈↓ α∧␈↓␈↓ αTThere␈α
may␈α
still␈α
be␈α
a␈α
bug␈α
in␈α
the␈α
S␈α
and␈α
P␈α
axioms,␈α
since␈α
the␈α
proof␈α
has␈α
not␈α
been␈α
carried␈α
out␈α
on
␈↓ α∧␈↓the computer.

␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305

␈↓ α∧␈↓ARPANET: MCCARTHY@SU-AI

␈↓ α∧␈↓␈↓ αT␈↓εThis draft of KNOW[E78,JMC] PUBbed at 9:11 on August 3, 1983.␈↓